| Definitions | True, t  T, "$x", Id, P   Q, False,  A, A B,  , {x:A| B(x) },  , s = t, Prop,  , Void, Knd, rcv(l,tg), x : v, KindDeq, f  g, f(x)?z, Type, Unit, a<b, @loc precondition for a(v:T):P State(ds) v, DeclaredType(ds;x), n+m, @loc effect knd(v:T) x := f State(ds) v , <a,b>, nil, car.cdr, sends knd(v:T) on l:tagged(g,State(ds),v):dt, , Atom, left right, R-da(R;i), x:A  B(x),  x:A. B(x), P  Q, x:A B(x),  b, P & Q, P Q, Top,  x:A. B(x), Valtype(da;k), lnk$n{$a to $b}, IdLnk, IdDeq, State(ds), f(a),  x.A(x),  x. t(x), type List, locl(a), #$n, A & B, left+right, (x l), lnk_rcv{lnk_rcv_compseq_tag_def:ObjectId}(tg; l), isrcv_rcv{isrcv_rcv_compseq_tag_def:ObjectId}(tg; l), source(l), destination(l), hd(l), i<j, ij, l[i], tl(l), ||as||, isrcv(k), lnk(k), {T}, SQType(T), s ~ t, P  Q, Dec(P),  x:A. B(x), xL. P(x), Atom$n, rec(x.A(x)), Realizer, EqDecider(T), es realizer ind, R-Feasible(R), '$x'2, x,y. t(x;y), update-spec1(k;x;n;s,v.f(s;v)), Case b of inl(x) s(x) ; inr(y) t(y), if b t else f fi, 2of(t), a:A fp B(a), update-spec(ds;da), a b, true, rcv_rcv{rcv_rcv_compseq_tag_def:ObjectId}(t'; l'; t; l), eq_atom$n(x;y), Atom2Deq, eqof(d), a = b, proddeq(a;b), product-deq(A;B;a;b), IdLnkDeq, a = b, k sends on l with tag tg [s,v.f(s;v)], at marker n, msg-item(ds;da;k;l), msg-spec(ds;da), eclbase(k;test), ecl(ds;da), a.n, eclseq(a;b), es realizer ind Rsends compseq tag def, es realizer ind Rplus compseq tag def, es realizer ind Reffect compseq tag def, es realizer ind Rpre compseq tag def, R-has-loc(R;i), isrcv_locl{isrcv_locl_compseq_tag_def:ObjectId}(a), f || g, lnk-decl(l;dt), i=j, Rsends-T(x1), Rsends-dt(x1), Rsends-l(x1), Rsends-knd(x1), Rsends?(x1), Reffect-T(x1), Reffect-knd(x1), Reffect?(x1), Rrframe-L(x1), Rpre-a(x1), Rpre-ds(x1), Rrframe-x(x1), Rrframe?(x1), Rpre?(x1), Rsends-ds(x1), Rbframe-L(x1), Rbframe-k(x1), Rbframe?(x1), Rsframe-L(x1), Rsends-g(x1), Rsframe-tag(x1), Rsframe-lnk(x1), Rsframe?(x1), Reffect-ds(x1), Raframe-L(x1), Reffect-x(x1), Raframe-k(x1), Raframe?(x1), Rframe-L(x1), Rframe-x(x1), Rframe?(x1), Rnone?(x1), Rplus-right(x1), Rplus-left(x1), Rplus?(x1), R-interface-compat(A;B), R-frame-compat(A;B), p = q, R-base-domain(R), Rda(R), Rds(R), R-loc(R), inr(x), b, rcv_locl{rcv_locl_compseq_tag_def:ObjectId}(a; tg; l), tag_rcv{tag_rcv_compseq_tag_def:ObjectId}(tg; l), Normal(ds), AtomFree(T;x),  , Normal(T), "$token", ecl-machine at i with state $eclAstate variables dsactions dasends sndupdates upd |
| Lemmas | ecl-feasible, normal-da-join, normal-da-single, decidable ex unit, decidable lt, R-Feasible-Rplus, bool-inhabited, it wf, fpf-all-empty, normal-ds-single, fpf-empty-compatible-right, fpf-compatible-join, lnk-decls-compatible, fpf-compatible-self, R-compat-Rplus-sq, assert-eq-knd, R-compat-disjoint, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, bnot wf, not wf, eq id wf, Id sq, fpf-empty-compatible-left, fpf-compatible-join2, lnk-decl wf, fpf-compatible-singles, fpf-compatible-symmetry, lnk-decl-compatible-single, R-compat-symmetry, ecl-disjoint-compatible, false wf, eclseq wf, eclact wf, eclbase wf, lt int wf, msg-spec1 wf, btrue wf, update-spec-join wf, ma-valtype wf, update-spec1 wf, fpf-join-cap-sq, fpf-single-dom-sq, update-spec-join-decl, update-spec1-decl, update-spec1 wf2, le wf, msg-spec-loc-decl-spec1, fpf-join wf, fpf-cap-single, eqof eq btrue, subtype rel self, deq wf, Knd sq, decidable int equal, lsrc wf, ldst wf, lnk wf, assert wf, isrcv wf, select wf, length wf1, l member wf, IdLnk wf, fpf-cap wf, Knd wf, R-da wf, Rpre wf, Reffect wf, locl wf, Rplus wf, Rsends wf, fpf-cap-single1, id-deq wf, decl-state wf, fpf-empty wf, decl-type wf, fpf-single wf, unit wf, Kind-deq wf, rcv wf, top wf, assert-eq-id, bool wf, Id wf, true wf |
@"a"